feat: finite sets are closed under directed suprema by vihdzp · Pull Request #39724 · leanprover-community/mathlib4

vihdzp · 2026-05-22T22:20:31Z

As are chains of length ≤ ω.

We don't prove Set.Finite.dirSupClosed via DirectedOn.finite_le, in order to save a few imports.

github-actions · 2026-05-22T22:21:45Z

PR summary 16b1cd464d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.SetTheory.Cardinal.Cofinality.Ordinal	746	760	+14 (+1.88%)

Import changes for all files

Files	Import difference
`Mathlib.Order.DirSupClosed`	-379
1911 files `Mathlib.Algebra.AffineMonoid.Embedding` `Mathlib.Algebra.AffineMonoid.UniqueSums` `Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder` `Mathlib.Algebra.Algebra.Subalgebra.Rank` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Algebra.Azumaya.Basic` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Category.CommAlgCat.FiniteType` `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.FGModuleCat.Abelian` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Colimits` `Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Descent` `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Ext.Basic` `Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting` `Mathlib.Algebra.Category.ModuleCat.Ext.Finite` `Mathlib.Algebra.Category.ModuleCat.Ext.HasExt` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.Ring.EqualizerPushout` `Mathlib.Algebra.Category.Ring.FinitePresentation` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Small` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Category.Ring.Under.Property` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Exact.Sequence` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear` `Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Map` `Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure` `Mathlib.Algebra.Homology.DerivedCategory.Fractions` `Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.KInjective` `Mathlib.Algebra.Homology.DerivedCategory.KProjective` `Mathlib.Algebra.Homology.DerivedCategory.Linear` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom` `Mathlib.Algebra.Homology.DerivedCategory.TStructure` `Mathlib.Algebra.Homology.Factorizations.CM5a` `Mathlib.Algebra.Homology.HomotopyCategory.Acyclic` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.KInjective` `Mathlib.Algebra.Homology.HomotopyCategory.KProjective` `Mathlib.Algebra.Homology.HomotopyCategory.Plus` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.Algebra.Homology.ModelCategory.Injective` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.AdjointAction.Basic` `Mathlib.Algebra.Lie.AdjointAction.Derivation` `Mathlib.Algebra.Lie.AdjointAction.JordanChevalley` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Basis` `Mathlib.Algebra.Lie.CartanCriterion` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Cochain` `Mathlib.Algebra.Lie.Derivation.BaseChange` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.Graded` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Loop` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Prod` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.SemiDirect` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.SerreConstruction` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Algebra.Lie.Sl2` `Mathlib.Algebra.Lie.Solvable` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.IsSimple` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.LieRinehartAlgebra.Defs` `Mathlib.Algebra.LieRinehartAlgebra.Subalgebra` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LinearMap.FiniteRange` `Mathlib.Algebra.Module.LinearMap.Index` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Algebra.Module.SpanRankOperations` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.Module.StablyFree.Basic` `Mathlib.Algebra.Module.StablyFree.FreeOfInvertible` `Mathlib.Algebra.Module.Submodule.Union` `Mathlib.Algebra.Module.Torsion.PrimaryComponent` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Algebra.Module.ZLattice.Summable` `Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.Algebra.Polynomial.Sequence` `Mathlib.Algebra.QuadraticAlgebra.Basic` `Mathlib.Algebra.QuadraticAlgebra.Defs` `Mathlib.Algebra.QuadraticAlgebra.NormDeterminant` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Star.LinearMap` `Mathlib.Algebra.Symmetrized` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.AlgClosed.Basic` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.Birational.Dominant` `Mathlib.AlgebraicGeometry.Birational.RationalMap` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.EffectiveEpi` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.LFunction` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Geometrically.Basic` `Mathlib.AlgebraicGeometry.Geometrically.Connected` `Mathlib.AlgebraicGeometry.Geometrically.Integral` `Mathlib.AlgebraicGeometry.Geometrically.Irreducible` `Mathlib.AlgebraicGeometry.Geometrically.Reduced` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Group.Smooth` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.FlatRank` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.AffineEtale` `Mathlib.AlgebraicGeometry.Sites.Affine` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.ConstantSheaf` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicGeometry.Sites.EtalePoint` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Fpqc` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.Proetale` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct` `Mathlib.Analysis.AbsoluteValue.Equivalence` `Mathlib.Analysis.Analytic.Binomial` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.Extreme` `Mathlib.Analysis.CStarAlgebra.Fuglede` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.Projection` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitary.Connected` `Mathlib.Analysis.CStarAlgebra.Unitary.Span` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox` `Mathlib.Analysis.Calculus.ContDiff.Convolution` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.ImplicitContDiff` `Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate` `Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.LogDerivUniformlyOn` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.TaylorIntegral` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.BorelCaratheodory` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.Harmonic.Analytic` `Mathlib.Analysis.Complex.Harmonic.Liouville` `Mathlib.Analysis.Complex.Harmonic.MeanValue` `Mathlib.Analysis.Complex.Harmonic.Poisson` `Mathlib.Analysis.Complex.HasPrimitives` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.JensenFormula` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.MeanValue` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Poisson` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.GaussLucas` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.SummableUniformlyOn` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Measure` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction` `Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.Complex.ValueDistribution.Cartan` `Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction` `Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem` `Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic` `Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic` `Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic` `Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Approximation` `Mathlib.Analysis.Convex.BetweenList` `Mathlib.Analysis.Convex.Between` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Cone.Dual` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.TensorProduct` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.DoublyStochasticMatrix` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convex.Radon` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.Visible` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.ContDiffMapSupportedIn` `Mathlib.Analysis.Distribution.DerivNotation` `Mathlib.Analysis.Distribution.Distribution` `Mathlib.Analysis.Distribution.FourierMultiplier` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace.Basic` `Mathlib.Analysis.Distribution.SchwartzSpace.Deriv` `Mathlib.Analysis.Distribution.SchwartzSpace.Fourier` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Distribution.Sobolev` `Mathlib.Analysis.Distribution.Support` `Mathlib.Analysis.Distribution.TemperateGrowth` `Mathlib.Analysis.Distribution.TemperedDistribution` `Mathlib.Analysis.Distribution.TestFunction` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.Convolution` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.LpSpace` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.CanonicalTensor` `Mathlib.Analysis.InnerProductSpace.Coalgebra` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.GramMatrix` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Analysis.InnerProductSpace.Harmonic.Basic` `Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions` `Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Laplacian` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.MulOpposite` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection.Basic` `Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional` `Mathlib.Analysis.InnerProductSpace.Projection.Reflection` `Mathlib.Analysis.InnerProductSpace.Projection.Submodule` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Reproducing` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.SingularValues` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StandardSubspace` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.TensorProduct` `Mathlib.Analysis.InnerProductSpace.Trace` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LocallyConvex.HahnBanach` `Mathlib.Analysis.LocallyConvex.Montel` `Mathlib.Analysis.LocallyConvex.SeparatingDual` `Mathlib.Analysis.LocallyConvex.Separation` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WeakOperatorTopology` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.Matrix.Hermitian` `Mathlib.Analysis.Matrix.LDL` `Mathlib.Analysis.Matrix.Normed` `Mathlib.Analysis.Matrix.Order` `Mathlib.Analysis.Matrix.PosDef` `Mathlib.Analysis.Matrix.Spectrum` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Meromorphic.Complex` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.AsymptoticCone` `Mathlib.Analysis.Normed.Affine.Convex` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.GelfandFormula` `Mathlib.Analysis.Normed.Algebra.GelfandMazur` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Field.Dense` `Mathlib.Analysis.Normed.Field.Krasner` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.Normed.Lp.Matrix` `Mathlib.Analysis.Normed.Lp.SmoothApprox` `Mathlib.Analysis.Normed.Module.Bases` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.Normed.Module.Connected` `Mathlib.Analysis.Normed.Module.ContinuousInverse` `Mathlib.Analysis.Normed.Module.DoubleDual` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.HahnBanach` `Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension` `Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative` `Mathlib.Analysis.Normed.Operator.CompleteCodomain` `Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv` `Mathlib.Analysis.Normed.Operator.FredholmAlternative` `Mathlib.Analysis.Normed.Ring.InfiniteProd` `Mathlib.Analysis.Normed.Unbundled.FiniteExtension` `Mathlib.Analysis.Normed.Unbundled.InvariantExtension` `Mathlib.Analysis.Normed.Unbundled.SpectralNorm` `Mathlib.Analysis.ODE.ExistUnique` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Factorization` `Mathlib.Analysis.Polynomial.Fourier` `Mathlib.Analysis.Polynomial.MahlerMeasure` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.Real.Hyperreal` `Mathlib.Analysis.Real.Pi.Chudnovsky` `Mathlib.Analysis.Real.Pi.Irrational` `Mathlib.Analysis.Real.Pi.Leibniz` `Mathlib.Analysis.Real.Pi.Wallis` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` `Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gamma.Digamma` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrability.Basic` `Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic` `Mathlib.Analysis.SpecialFunctions.Integrals.Basic` `Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric` `Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Sigmoid` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecificLimits.Fibonacci` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.SumIntegralExpDecay` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.Injective.Dimension` `Mathlib.CategoryTheory.Abelian.Injective.Ext` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Projective.Ext` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris` `Mathlib.CategoryTheory.Triangulated.Adjunction` `Mathlib.CategoryTheory.Triangulated.Generators` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory` `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.OpOp` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated` `Mathlib.CategoryTheory.Triangulated.Orthogonal` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc` `Mathlib.CategoryTheory.Triangulated.TStructure.Induced` `Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject` `Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT` `Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Data.Nat.Choose.Lucas` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.AddCircleAdd` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Dynamics.Ergodic.Extreme` `Mathlib.Dynamics.Ergodic.RadonNikodym` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.Extension` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Finite.Valuation` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.IntermediateField.ExtendRight` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.FieldTheory.Minpoly.ConjRootClass` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Minpoly.Finite` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.MvRatFunc.Rank` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.RatFunc.Valuation` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SeparablyGenerated` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.Convex.Cone.TensorProduct` `Mathlib.Geometry.Diffeology.Basic` `Mathlib.Geometry.Euclidean.Altitude` `Mathlib.Geometry.Euclidean.Angle.Bisector` `Mathlib.Geometry.Euclidean.Angle.Incenter` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Oriented.Projection` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Congruence` `Mathlib.Geometry.Euclidean.Incenter` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.NinePointCircle` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Euclidean.Projection` `Mathlib.Geometry.Euclidean.SignedDist` `Mathlib.Geometry.Euclidean.Similarity` `Mathlib.Geometry.Euclidean.Simplex` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.OrthRadius` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Sphere.Tangent` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Euclidean.Volume.Measure` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SMul` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.Bordism` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Constructions` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.GroupLieAlgebra` `Mathlib.Geometry.Manifold.Immersion` `Mathlib.Geometry.Manifold.Instances.Icc` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.Notation` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Riemannian.Basic` `Mathlib.Geometry.Manifold.Riemannian.PathELength` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.SmoothApprox` `Mathlib.Geometry.Manifold.SmoothEmbedding` `Mathlib.Geometry.Manifold.Submersion` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.LocalFrame` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.Riemannian` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorBundle.Tensoriality` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.Geometry.Polygon.Basic` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.GroupTheory.IndexNSmul` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.ChainRule` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.MulOpposite` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.LinearAlgebra.Center` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.CliffordAlgebra.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation` `Mathlib.LinearAlgebra.CliffordAlgebra.Contraction` `Mathlib.LinearAlgebra.CliffordAlgebra.Equivs` `Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv` `Mathlib.LinearAlgebra.CliffordAlgebra.Even` `Mathlib.LinearAlgebra.CliffordAlgebra.Fold` `Mathlib.LinearAlgebra.CliffordAlgebra.Grading` `Mathlib.LinearAlgebra.CliffordAlgebra.Inversion` `Mathlib.LinearAlgebra.CliffordAlgebra.Prod` `Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup` `Mathlib.LinearAlgebra.CliffordAlgebra.Star` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.LinearAlgebra.Complex.Determinant` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.LinearAlgebra.Complex.Orientation` `Mathlib.LinearAlgebra.Contraction` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.LinearAlgebra.Dimension.OrzechProperty` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.Dual.BaseChange` `Mathlib.LinearAlgebra.Dual.Lemmas` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Charpoly` `Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basis` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.LinearAlgebra.ExteriorPower.Basic` `Mathlib.LinearAlgebra.ExteriorPower.Basis` `Mathlib.LinearAlgebra.ExteriorPower.Pairing` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient` `Mathlib.LinearAlgebra.FreeModule.Finite.Matrix` `Mathlib.LinearAlgebra.FreeModule.Finite.Quotient` `Mathlib.LinearAlgebra.FreeModule.IdealQuotient` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.LinearAlgebra.FreeModule.ModN` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.LinearAlgebra.Matrix.BaseChange` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.LinearAlgebra.Matrix.Block` `Mathlib.LinearAlgebra.Matrix.Charpoly.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff` `Mathlib.LinearAlgebra.Matrix.Charpoly.Disc` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.Rank` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.LinearAlgebra.Matrix.Stochastic` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.LinearAlgebra.Matrix.WithConv` `Mathlib.LinearAlgebra.Matrix.ZMatrix` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.LinearAlgebra.Multilinear.FiniteDimensional` `Mathlib.LinearAlgebra.Orientation` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.PerfectPairing.Basic` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.PiTensorProduct.Dual` `Mathlib.LinearAlgebra.Projectivization.Action` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Collinear` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.LinearAlgebra.QuadraticForm.AlgClosed` `Mathlib.LinearAlgebra.QuadraticForm.Basic` `Mathlib.LinearAlgebra.QuadraticForm.Basis` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv` `Mathlib.LinearAlgebra.QuadraticForm.Isometry` `Mathlib.LinearAlgebra.QuadraticForm.Prod` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.LinearAlgebra.QuadraticForm.Radical` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.QuadraticForm.Signature` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.Reflection` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.BaseExists` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.LinearAlgebra.SesquilinearForm.Star` `Mathlib.LinearAlgebra.Span.TensorProduct` `Mathlib.LinearAlgebra.SpecialLinearGroup` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basis` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.LinearAlgebra.Trace` `Mathlib.LinearAlgebra.Transvection.Basic` `Mathlib.LinearAlgebra.Transvection` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.LinearAlgebra.Vandermonde` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.AbsolutelyContinuous` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner` `Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut` `Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.ConditionalLExpectation` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.MeasureTheory.Function.ConvergenceInDistribution` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.MeasureTheory.Function.Holder` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.JacobianOneDim` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L1Space.AEEqFun` `Mathlib.MeasureTheory.Function.L1Space.Integrable` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm` `Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.IntegralConvolution` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.MeasureTheory.Group.ModularCharacter` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.Bochner.Basic` `Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap` `Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Bochner.L1` `Mathlib.MeasureTheory.Integral.Bochner.Set` `Mathlib.MeasureTheory.Integral.Bochner.SumMeasure` `Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.MeasureTheory.Integral.CircleAverage` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.CompactlySupported` `Mathlib.MeasureTheory.Integral.CurveIntegral.Basic` `Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.FinMeasAdditive` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral` `Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm` `Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope` `Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.MeanValue` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.Regular` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion` `Mathlib.MeasureTheory.Measure.CharacteristicFunction` `Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.FiniteMeasureExt` `Mathlib.MeasureTheory.Measure.FiniteMeasurePi` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.DistribChar` `Mathlib.MeasureTheory.Measure.Haar.Extension` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.MeasureTheory.Measure.IntegralCharFun` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.MeasureTheory.Measure.LevyConvergence` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Prokhorov` `Mathlib.MeasureTheory.Measure.ResolventTransform` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Measure.TightNormed` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero` `Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap` `Mathlib.MeasureTheory.SpecificCodomains.Pi` `Mathlib.MeasureTheory.SpecificCodomains.WithLp` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.VectorMeasure.Integral` `Mathlib.MeasureTheory.VectorMeasure.SetIntegral` `Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.ArithmeticFunction.Carmichael` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.Chebyshev` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DiophantineApproximation.Basic` `Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.FLT.Polynomial` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.Height.Projectivization` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.Complex` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LocalField.Basic` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.BoundedAtCusp` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.ModularForms.CuspFormSubmodule` `Mathlib.NumberTheory.ModularForms.Cusps` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LevelOne.Basic` `Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula` `Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.Niven` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.InfinitePlace` `Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.ExistsRamified` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.AddChar` `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.NumberTheory.Pell` `Mathlib.NumberTheory.PowModTotient` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Inertia` `Mathlib.NumberTheory.RamificationInertia.Ramification` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RamificationInertia.Valuation` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.NumberTheory.Rayleigh` `Mathlib.NumberTheory.Real.GoldenRatio` `Mathlib.NumberTheory.Real.Irrational` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.ZetaValues` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.BrownianMotion.Basic` `Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily` `Mathlib.Probability.CDF` `Mathlib.Probability.CentralLimitTheorem` `Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.Decision.BayesEstimator` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Bernoulli` `Mathlib.Probability.Distributions.Beta` `Mathlib.Probability.Distributions.Binomial` `Mathlib.Probability.Distributions.Cauchy` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Fernique` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian.Basic` `Mathlib.Probability.Distributions.Gaussian.CharFun` `Mathlib.Probability.Distributions.Gaussian.Fernique` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence` `Mathlib.Probability.Distributions.Gaussian.Multivariate` `Mathlib.Probability.Distributions.Gaussian.Real` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Poisson.Basic` `Mathlib.Probability.Distributions.Poisson.PoissonLimitThm` `Mathlib.Probability.Distributions.SetBernoulli` `Mathlib.Probability.Distributions.TwoValued` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.HasCondDistrib` `Mathlib.Probability.HasLawExists` `Mathlib.Probability.HasLaw` `Mathlib.Probability.IdentDistribIndep` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.BoundedContinuousFunction` `Mathlib.Probability.Independence.CharacteristicFunction` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.InfinitePi` `Mathlib.Probability.Independence.Integrable` `Mathlib.Probability.Independence.Integration` `Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic` `Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess` `Mathlib.Probability.Independence.Process.HasIndepIncrements` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.RadonNikodym` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.Integral` `Mathlib.Probability.Kernel.IonescuTulcea.Traj` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Kernel.Representation` `Mathlib.Probability.Kernel.SetIntegral` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.Basic` `Mathlib.Probability.Moments.ComplexMGF` `Mathlib.Probability.Moments.CovarianceBilinDual` `Mathlib.Probability.Moments.CovarianceBilin` `Mathlib.Probability.Moments.Covariance` `Mathlib.Probability.Moments.IntegrableExpMul` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Moments.Tilted` `Mathlib.Probability.Moments.Variance` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.FiniteDimensionalLaws` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.LocalProperty` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Predictable` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.ProductMeasure` `Mathlib.Probability.StrongLaw` `Mathlib.RepresentationTheory.Action` `Mathlib.RepresentationTheory.AlgebraRepresentation.Basic` `Mathlib.RepresentationTheory.Basic` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.Coinduced` `Mathlib.RepresentationTheory.Coinvariants` `Mathlib.RepresentationTheory.Continuous.Basic` `Mathlib.RepresentationTheory.Continuous.TopRep` `Mathlib.RepresentationTheory.Equiv` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.FinGroupCharZero` `Mathlib.RepresentationTheory.FiniteIndex` `Mathlib.RepresentationTheory.Homological.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro` `Mathlib.RepresentationTheory.Homological.GroupHomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro` `Mathlib.RepresentationTheory.Homological.Resolution` `Mathlib.RepresentationTheory.Homological.TateCohomology.Basic` `Mathlib.RepresentationTheory.Induced` `Mathlib.RepresentationTheory.Intertwining` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Irreducible` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RepresentationTheory.Rep.Basic` `Mathlib.RepresentationTheory.Rep.Iso` `Mathlib.RepresentationTheory.Rep.Res` `Mathlib.RepresentationTheory.Semisimple` `Mathlib.RepresentationTheory.Submodule` `Mathlib.RepresentationTheory.Subrepresentation` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Completeness` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.Adjoin.FGBaseChange` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.Adjoin.Polynomial.Bivariate` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.Algebraic.Basic` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.Algebraic.MvPolynomial` `Mathlib.RingTheory.Algebraic.StronglyTranscendental` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.AlgebraicIndependent.Transcendental` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Bialgebra.GroupLike` `Mathlib.RingTheory.ClassGroup.Basic` `Mathlib.RingTheory.ClassGroup.ExtendedHom` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Coalgebra.GroupLike` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.Conductor` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.Ideal.Basic` `Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas` `Mathlib.RingTheory.DedekindDomain.Instances` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.DividedPowers.Padic` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Descent` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Locus` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.Etale.StandardEtale` `Mathlib.RingTheory.Etale.Weakly` `Mathlib.RingTheory.Extension.Basic` `Mathlib.RingTheory.Extension.Cotangent.BaseChange` `Mathlib.RingTheory.Extension.Cotangent.Basic` `Mathlib.RingTheory.Extension.Cotangent.Basis` `Mathlib.RingTheory.Extension.Cotangent.Free` `Mathlib.RingTheory.Extension.Cotangent.LocalizationAway` `Mathlib.RingTheory.Extension.ExtendScalars` `Mathlib.RingTheory.Extension.Generators` `Mathlib.RingTheory.Extension.Presentation.Basic` `Mathlib.RingTheory.Extension.Presentation.Core` `Mathlib.RingTheory.Extension.Presentation.Submersive` `Mathlib.RingTheory.Filtration` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.FinitePresentation` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.FiniteType` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Cofinite` `Mathlib.RingTheory.Finiteness.Descent` `Mathlib.RingTheory.Finiteness.FinitePresentationLocal` `Mathlib.RingTheory.Finiteness.FiniteTypeLocal` `Mathlib.RingTheory.Finiteness.ModuleFinitePresentation` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.Finiteness.Quotient` `Mathlib.RingTheory.Finiteness.Small` `Mathlib.RingTheory.Flat.Basic` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Flat.Domain` `Mathlib.RingTheory.Flat.Equalizer` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra` `Mathlib.RingTheory.Flat.FaithfullyFlat.Basic` `Mathlib.RingTheory.Flat.FaithfullyFlat.Descent` `Mathlib.RingTheory.Flat.IsBaseChange` `Mathlib.RingTheory.Flat.Localization` `Mathlib.RingTheory.Flat.Rank` `Mathlib.RingTheory.Flat.Stability` `Mathlib.RingTheory.Flat.Tensor` `Mathlib.RingTheory.Flat.TorsionFree` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.FractionalIdeal.Inverse` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.GradedAlgebra.FiniteType` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.HopfAlgebra.GroupLike` `Mathlib.RingTheory.HopkinsLevitzki` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.AssociatedPrime.Localization` `Mathlib.RingTheory.Ideal.CotangentBaseChange` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Height` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.KrullsHeightTheorem` `Mathlib.RingTheory.Ideal.MinimalPrime.Colon` `Mathlib.RingTheory.Ideal.NatInt` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Ideal.Pure` `Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Ideal` `Mathlib.RingTheory.IntegralClosure.GoingDown` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.Jacobson.Artinian` `Mathlib.RingTheory.Jacobson.Polynomial` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.KrullDimension.LocalRing` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.NonZeroDivisors` `Mathlib.RingTheory.KrullDimension.PID` `Mathlib.RingTheory.KrullDimension.Polynomial` `Mathlib.RingTheory.KrullDimension.Regular` `Mathlib.RingTheory.KrullDimension.Zero` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LinearDisjoint` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalIso` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.FinitePresentation` `Mathlib.RingTheory.LocalProperties.InjectiveDimension` `Mathlib.RingTheory.LocalProperties.Injective` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.ProjectiveDimension` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalProperties.Semilocal` `Mathlib.RingTheory.LocalRing.Etale` `Mathlib.RingTheory.LocalRing.Length` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Square` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.LocalRing.Quotient` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Fiber` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.LocalRing.ResidueField.Instances` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.AtPrime.Extension` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.RingTheory.Localization.Free` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.MvPolynomial.Expand` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.RingTheory.MvPolynomial` `Mathlib.RingTheory.MvPowerSeries.Equiv` `Mathlib.RingTheory.MvPowerSeries.Expand` `Mathlib.RingTheory.Nilpotent.GeometricallyReduced` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.Norm.Defs` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.NormalClosure` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.OrderOfVanishing.Basic` `Mathlib.RingTheory.OrderOfVanishing.Noetherian` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Perfectoid.BDeRham` `Mathlib.RingTheory.Perfectoid.FontaineTheta` `Mathlib.RingTheory.Perfectoid.Untilt` `Mathlib.RingTheory.PicardGroup` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.RingTheory.Polynomial.Chebyshev` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.DegreeLT` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.IsIntegral` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.Resultant.Basic` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.RingTheory.Polynomial.UniversalFactorizationRing` `Mathlib.RingTheory.PolynomialLaw.Basic` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Exp` `Mathlib.RingTheory.PowerSeries.Expand` `Mathlib.RingTheory.PowerSeries.Ideal` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.PowerSeries.Log` `Mathlib.RingTheory.PowerSeries.WeierstrassPreparation` `Mathlib.RingTheory.QuasiFinite.Basic` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.QuasiFinite.Weakly` `Mathlib.RingTheory.RamificationInertia.Basic` `Mathlib.RingTheory.RamificationInertia.Inertia` `Mathlib.RingTheory.RamificationInertia.Ramification` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.RingTheory.Regular.Depth` `Mathlib.RingTheory.Regular.Flat` `Mathlib.RingTheory.Regular.Free` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.Regular.LinearMap` `Mathlib.RingTheory.Regular.ProjectiveDimension` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.RegularLocalRing.Defs` `Mathlib.RingTheory.RingHom.Bijective` `Mathlib.RingTheory.RingHom.EssFiniteType` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.FaithfullyFlat` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.OpenImmersion` `Mathlib.RingTheory.RingHom.PurelyInseparable` `Mathlib.RingTheory.RingHom.QuasiFinite` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.SimpleModule.IsAlgClosed` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.SimpleModule.WedderburnArtin` `Mathlib.RingTheory.Smooth.AdicCompletion` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Field` `Mathlib.RingTheory.Smooth.Flat` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.NoetherianDescent` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.Quotient` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Maximal.Localization` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` `Mathlib.RingTheory.Spectrum.Prime.Chevalley` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.LTSeries` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.RingTheory.Spectrum.Prime.RingHom` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Support` `Mathlib.RingTheory.Teichmuller` `Mathlib.RingTheory.TensorProduct.DirectLimitFG` `Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight` `Mathlib.RingTheory.TensorProduct.IsBaseChangeHom` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.TotallySplit` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Dedekind` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.FiniteField` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.IsTrivialOn` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.TeichmullerSeries` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.RingTheory.ZMod.Torsion` `Mathlib.RingTheory.ZMod.UnitsCyclic` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.NormNum.Irrational` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.AsymptoticCone` `Mathlib.Topology.Algebra.Group.Matrix` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.TopDualPairing` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.Algebra.Star.LinearMap` `Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Compactification.OnePoint.ProjectiveLine` `Mathlib.Topology.Compactification.OnePoint.Sphere` `Mathlib.Topology.Instances.AddCircle.DenseSubgroup` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.Instances.Irrational` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.Instances.RatLemmas` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.VectorBundle.FiniteDimensional`	2
`Mathlib.AlgebraicTopology.SimplicialSet.Presentable`	9
`Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator` `Mathlib.Order.Filter.Cocardinal`	10
6 files `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives` `Mathlib.CategoryTheory.Presentable.OrthogonalReflection` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.Order.Filter.CardinalInter` `Mathlib.SetTheory.Cardinal.Pigeonhole`	11
36 files `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Abelian.Subcategory` `Mathlib.CategoryTheory.Comma.CardinalArrow` `Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT` `Mathlib.CategoryTheory.MorphismProperty.Ind` `Mathlib.CategoryTheory.ObjectProperty.ClosureShift` `Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure` `Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure` `Mathlib.CategoryTheory.ObjectProperty.FiniteProducts` `Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT` `Mathlib.CategoryTheory.ObjectProperty.Ind` `Mathlib.CategoryTheory.ObjectProperty.LimitsClosure` `Mathlib.CategoryTheory.Presentable.Adjunction` `Mathlib.CategoryTheory.Presentable.Basic` `Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset` `Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation` `Mathlib.CategoryTheory.Presentable.ColimitPresentation` `Mathlib.CategoryTheory.Presentable.Dense` `Mathlib.CategoryTheory.Presentable.Directed` `Mathlib.CategoryTheory.Presentable.EssentiallyLarge` `Mathlib.CategoryTheory.Presentable.Finite` `Mathlib.CategoryTheory.Presentable.IsCardinalFiltered` `Mathlib.CategoryTheory.Presentable.Limits` `Mathlib.CategoryTheory.Presentable.LocallyPresentable` `Mathlib.CategoryTheory.Presentable.Presheaf` `Mathlib.CategoryTheory.Presentable.Retracts` `Mathlib.CategoryTheory.Presentable.StrongGenerator` `Mathlib.CategoryTheory.Presentable.Type` `Mathlib.CategoryTheory.SmallRepresentatives` `Mathlib.CategoryTheory.Subobject.HasCardinalLT` `Mathlib.MeasureTheory.MeasurableSpace.Card` `Mathlib.SetTheory.Cardinal.Cofinality.Ordinal` `Mathlib.SetTheory.Cardinal.HasCardinalLT` `Mathlib.SetTheory.Cardinal.Regular` `Mathlib.SetTheory.Ordinal.FundamentalSequence`	14
`Mathlib.Order.DirSupClosed.Basic`	379
`Mathlib.Order.DirSupClosed.Finite` (new file)	568

Declarations diff (regex)

+ DirSupClosed.singleton
+ DirSupClosedOn.singleton
+ DirectedOn.finite_le
+ IsClub.isStationary
+ IsCofinal.nonempty
+ IsStationary
+ IsStationary.mono
+ IsStationary.nonempty
+ IsStationary.of_not_isCofinal_compl
+ IsStationary.univ
+ Set.Finite.dirSupClosed
+ _root_.isClub_empty_iff
+ dirSupClosed_of_type_le_omega0
+ dirSupClosed_range_nat
+ iInter_of_countable
+ isStationary_iUnion_iff
+ isStationary_iUnion_iff_of_cof_le_one
+ isStationary_iUnion_iff_of_countable
+ isStationary_iUnion_iff_of_orderTop
+ isStationary_sUnion_iff
+ isStationary_sUnion_iff_of_cof_le_one
+ isStationary_sUnion_iff_of_countable
+ isStationary_sUnion_iff_of_orderTop
+ isStationary_union_iff
+ isStationary_univ_iff
+ nonempty
+ not_isStationary_empty
+ not_isStationary_iff
+ not_isStationary_of_isEmpty
+ sInter_of_countable

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 16b1cd464d
Reference commit 8b068a6bd8

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

note: file Mathlib/Order/DirSupClosed.lean` was renamed to `Mathlib/Order/DirSupClosed/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

mathlib-merge-conflicts · 2026-05-26T03:54:48Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-06-05T02:25:57Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-06-23T00:14:26Z

This pull request has conflicts, please merge master and resolve them.

vihdzp added 2 commits May 22, 2026 16:07

finish

f5ca261

add result

a33cc54

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label May 22, 2026

vihdzp mentioned this pull request May 22, 2026

feat: stationary sets in countable cofinality orders #39725

Open

2 tasks

vihdzp added 4 commits May 22, 2026 16:37

reduce imports

eb59dc0

split

c727a02

split

8d9e99f

golf

84e1e9b

github-actions Bot added file-removed A Lean module was (re)moved without a `deprecated_module` annotation and removed large-import Automatically added label for PRs with a significant increase in transitive imports labels May 22, 2026

vihdzp added 5 commits May 22, 2026 16:53

have

1e4865e

start

415ba66

more

87bba65

finish

9acee7f

not using yet

3b05026

vihdzp added the t-order Order theory label May 22, 2026

vihdzp added 11 commits May 22, 2026 17:13

revert

e656067

more theorems

122721a

spacing

8de73c0

generalize

5b7dd80

evenmore

33bf921

suggestion

1d05495

suggestions

e7cb9be

suggestion

0746b29

merge

c2500f9

why is this here

a7301dc

Merge branch 'statminusminusminus' into statminusminus

5a8bb30

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2026

Merge branch 'master' into statminusminus

8e03fc5

vihdzp changed the title ~~feat: finite sets are closed under suprema~~ feat: finite sets are closed under directed suprema May 27, 2026

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 5, 2026

Merge branch 'master' into statminusminus

16b1cd4

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 21, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 23, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: finite sets are closed under directed suprema#39724

feat: finite sets are closed under directed suprema#39724
vihdzp wants to merge 24 commits into
leanprover-community:masterfrom
vihdzp:statminusminus

vihdzp commented May 22, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 22, 2026 •

edited

Loading

Import changes for modified files

Declarations diff (regex)

Uh oh!

mathlib-merge-conflicts Bot commented May 26, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jun 5, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jun 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

vihdzp commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 16b1cd464d

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- pending)

Uh oh!

mathlib-merge-conflicts Bot commented May 26, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jun 5, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jun 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

vihdzp commented May 22, 2026 •

edited

Loading

github-actions Bot commented May 22, 2026 •

edited

Loading